Step of Proof: subtype_rel-equal
11,40
postcript
pdf
Inference at
*
I
of proof for Lemma
subtype
rel-equal
:
A
,
B
:Type. (
A
=
B
)
(
A
r
B
)
latex
by Auto THEN D 0 THEN Auto
latex
.
Definitions
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
subtype
rel
wf
origin
A, B:Type. (A = B) 
(A 
r B)
by Auto THEN D 0 THEN Auto
. A, B:Type. (A = B) (A r B)
by Auto THEN D 0 THEN Auto
.
T Qx:A. B(x)